Module isotope::prelude [−][src]
Expand description
Commonly used items
Re-exports
pub use ctx::cons::ConsCtx; | |
pub use ctx::eq::Structural; | |
pub use ctx::eq::TermEqCtx; | |
pub use ctx::eq::TermEqCtxEdit; | |
pub use ctx::eq::TermEqCtxMut; | |
pub use ctx::eq::Typed; | |
pub use ctx::eq::Untyped; | |
pub use ctx::eval::Reduce; | |
pub use ctx::eval::ReductionConfig; | |
pub use ctx::subst::EvalCtx; | |
pub use ctx::subst::SubstCtx; | |
pub use ctx::ty::BinaryCtx; | |
pub use ctx::ty::Trivial; | |
pub use ctx::ty::TrivialCons; | |
pub use ctx::ty::TyCtxMut; | |
pub use ctx::ty::TRIVIAL; | |
pub use ctx::StandardCtx; | |
pub use program::NodeIx; | |
pub use term::dynamic::DynamicTerm; | |
pub use term::dynamic::DynamicValue; | |
pub use term::flags::AtomicTyckFlags; | |
pub use term::flags::TyckFlag; | |
pub use term::flags::TyckFlags; | |
pub use term::weak::WeakId; | |
pub use term::Cons; | |
pub use term::HasDependencies; | |
pub use term::Substitute; | |
pub use term::Term; | |
pub use term::TermEq; | |
pub use term::TermId; | |
pub use term::Typecheck; | |
pub use term::Value; |
Structs
Annotation | An owned type annotation |
App | A function application, with an optional type annotation |
Case | A case expression, which switches on variants to return a value |
DisjointSetCtx | A standard context for hash-consing and equality checking |
Enum | A type with a finite number of named variants |
Id | The identity type, representing proofs that two terms are equal |
Lambda | A lambda function |
NormalCfg | A reduction configuration to keep going until reaching a given form for up to |
Pi | A dependent function type |
ReduceUntil | A reduction configuration to keep going until a given condition has been reached, delegating otherwise to another configuration |
Refl | The reflexivity axiom: asserts that the left hand side and right hand side are judgementally equal, and therefore propositionally equal |
Shift | Shift a term up or down by an amount |
SubstSlice | A simple slice of substitutions |
SubstVec | A simple vector of substitutions |
Universe | A typing universe |
UniverseTerm | A term containing a typing universe |
Var | A variable, represented by a de-Bruijn index |
VarFilter | A filter for variables |
Variant | A variant of an enumeration |
Enums
AnnotationRef | A borrowed type annotation |
Form | Forms a term can be in |
Traits
AnnotationLike | A term which behaves like a (potentially borrowed) annotation |
OptionalValue | A convenience trait implemented by |